R1CS: A Day in the Life of a few Equations
An explainer post by @sunfishstanford
Introductionβ
zkSNARKs are beguiling in their potential power and scary in the complexity of the underlying math. The good news is there are now several well-written blogs and tutorials for the key aspects of zkSNARKs and their variants; however, there remain many difficult parts that are challenging for newcomers to grasp. This explainer post focuses on one key part of the zkSNARK stack: the R1CS protocol. We will go through a simple example in great detail, with minimal skipping of steps, to make it straightforward to follow along.
We will focus on the example used in Vitalik's great post, Quadratic Arithmetic Programs: from Zero to Hero.
Context: what is R1CS and how does it fit in?β
Here is an informal explanation of how zkSNARKs are used (or at least one common way they are used) and how R1CS fits in:
- A large class of computational tasks belong to the "NP complexity class", which means that the task is difficult to solve (meaning that as the size of the problem is increased, it becomes exponentially more difficult to solve), but is "easy" to verify (meaning that if a claimed solution is provided, the verification of that is computationally "cheap")
- However, the meaning of "easy" and "cheap" are relative, and in many cases it is still valuable to be able to verify in an even less computationally costly way. For example, if a large number of parties need to independently verify the same claimed solution, then it would be very valuable to have a way to pose the claimed solution so that it's very simple for each party to verify
- In other words, it may be valuable to add additional overhead to the posing of the claimed solution (done by the zkSNARK prover), in order to achieve large savings in the verification of the claimed solution (done by the zkSNARK verifier)
- Restated in a simpler way, the main idea is for one party to do a lot of work in order to save many other parties from having to repeat a lot of work, and thereby achieve net savings
- A meta thought: this is essentially what a teacher tries to do when coming up with clear, concise examples to enable students to more easily grasp the key concepts; in fact, that is what motivates this explainer post
- In pursuit of this direction, many different SNARK-related proof systems (each with pros and cons) have been invented, and it turns out that most of them rely on a protocol called "Rank-1 constraint satisfiability" (R1CS) to translate arbitrary computational tasks into a common mathematical description that can be fed into the proof system
- So the R1CS protocol is a powerful way to formally capture an algebraic circuit and to translate into a set of matrices and vectors that can be fed into a downstream proof system
Here is an example of a pipeline of steps behind a zkSNARK, as drawn by Eran Tromer and reproduced here from Vitalik's post:
As you can see in the figure and as explained in Vitalik's blog, the equation to be proved must first be expressed as a set of simple equations (which form "gates" that comprise an "algebraic circuit"). Next, the R1CS protocol enables the algebraic circuit to be expressed as a set of vectors and matrices, which then in turn are converted to a set of polynomials to be used in the QAP protocol, which then is fed to the rest of the zkSNARK pipeline.
For the rest of this post, we will focus on turning a simple "equation to be proved" (for our example, the equation to be proved is , which is satisfied via ) into a set of gates and then running that through the R1CS protocol.
Step 1: Flatteningβ
We start with what Vitalik calls "flattening", by transforming the equation into a sequence of simpler equations ("arithmetic gates") that each has at most one multiplication operation:
Note that each of these equations consists of an assignment of a variable (on the left) to an expression (on the right), where each expression is of the form or (where denotes multiplication). So there are two inputs and one output for each equation, and you can think of each equation as an "arithmetic gate", analogous to AND gates or XOR gates. For a zkSNARK, these arithmetic gate operations are defined on what's called a finite field (which is sort of like a finite version of the set of real numbers, so that you can freely add, subtract, multiply, and divide). Finite fields are part of the study of abstract algebra, and a finite field is an example of an "algebraic structure". This is probably why these combinations of arithmetic gates are called "algebraic circuits" -- they belong to a type of circuit, analogous to electronic circuits with AND gates or XOR gates, but they perform arithmetic operations on a finite field, hence the name "algebraic circuits."
Via algebraic substitution, working from the first equation through the last equation, we see that this set of four equations is equivalent to the original equation, as long as has the value of . This is shown via the animation here (remember that the original equation can be re-written as ):
So we've shown that the original equation, which has a single variable , is equivalent to the set of four arithmetic gates, which have the following five variables:
For the R1CS process, we will need one more "variable", (you could also think of it as a declared constant, with the value of 1). Let's list these six variable in the same order as Vitalik's post:
We already computed the values of the variables when we went through the algebraic substitution steps shown above. The following animation shows in more detail the transformation of the equations for the four gates into four concrete arithmetic equations:
Step 2: Gates to R1CSβ
Continuing along Vitalik's post, we come to our main topic. At this point, we have converted our computational task to the following four equations:
Just to reinforce the point, it's important to realize that if we can prove the correctness of these 4 equations, then that's equivalent to proving the original equation, , when . Why is that so? Because every step we've taken so far can be run backwards. For example, here is the previous animation run backwards:
The way to understand this reversed animation is to think of each of the variables (, , etc.) as a set of cards (a given variable can have several copies) where each card can either be face up, with the value showing (e.g., ), or face down, with the value hidden but the name of the variable showing (e.g. ). We must obey the following rules: (1) in the set of equations, each occurrence of the same variable must have the same consistent value (e.g., must always have the value wherever it appears), and (2) all of the arithmetic equations must be valid. So this animation clearly shows that these rules are satisfied when .
Vitalik's post shows an example of how to look at the gate, in the figure reproduced here:
Notice that the vertical columns with 1, 3, 35, etc., is the same set of values as our list of six variables (, , , etc.). This is called the witness, denoted by the vector , and it is the same for all our gates. The other part of R1CS consists of a triplet of vectors for each gate. Vitalik's post gives the values for these triplets for each of the four gates; let's work through how they are derived.
For a given arithmetic gate, if the witness is and the vector triplet is , then the gate's equation must be equivalent to . The vectors , , , and are all vectors, where is the number of variables in the algebraic circuit (in our case, ). This means that first is dot-product'ed with , which gives a scalar result. Similarly, the dot product of and gives a second scalar result, and the the dot product of and gives a third scalar result. Taking those three scalar results, we obtain the following equation: the product of the first two scalar results minus the third scalar result equals zero. This equation must be equivalent to the defining equation of the arithmetic gate. The animation below shows how to transform the first gate into its R1CS triplet vectors :
One way to interpret the meaning of the R1CS dot product equations is to think of the witness as a memory register that stores the values of all the relevant variables that take part in the four gates. Therefore, in order to reproduce a given gate, we think of the gate as a multiplier of two inputs to produce an output, and we specify a constraint on the system so that the product of the two inputs is equal to the output (i.e., if this constraint is satisfied, then the multiplier gate is operating correctly, which lets us reason "backwards" to eventually convince ourselves that the original "equation to be proved" must be correct). This is accomplished by using each of the triplet vectors as a "selector", with a at the position that corresponds to the desired variable held in the memory register . So in the case of the first gate, as the animation shows, the first input to the multiplier gate should be , and therefore the selector vector needs to have a in the second element (corresponding to the index of the variable in the witness vector ), and values of for all other elements. Similarly, the vector selects to be the second input to the multiplier gate, and the vector selects to be the output of the multiplier gate.
From the animation, we can see that the values of the triplet vectors for the first gate are highlighted in the blue boxes, and the results are
in agreement with the result in Vitalik's post.
The calculations for the second gate follow very similar steps. The third gate, however, is a bit different because there is an addition, but there does not seem to be a multiplication. But the way we handle it is to consider the equations as
So now we see the purpose of including the constant variable . We see that the selector vector selects for both and , and the mechanics of the dot product operation automatically gives us the sum of those two. The selector vector selects the variable , and the selector variable selects the variable . The animation below shows the details:
For the fourth gate, the calculation of is similar to the third gate, and we will leave its derivation to the reader as an exercise.
Conclusionβ
So there you have it: you have seen what's running "under the hood" of the machinery that calculates the R1CS vectors for an example algebraic circuit. When we break it down into the underlying elementary steps, you can see that it is no more complicated than some arithmetic along with a lot of careful bookkeeping.
I hope you have enjoyed this, and wish you a great journey digging deeper into the fascinating math behind zkSNARKs!
Acknowledgmentsβ
This project was done as part of 0xPARCβs ZK Identity Working Group in Spring 2022. Thanks to the Manim Community for the excellent Manim math animation library.